module Sol10  

where 

import SAU
import List

freeVarsInForm              :: Form -> [Id]
freeVarsInForm (Atom a ts) = (nub . concat . map varsInTerm) ts
freeVarsInForm (Neg form)  = freeVarsInForm form
freeVarsInForm (Impl form1 form2) = 
    nub ((freeVarsInForm form1) ++ (freeVarsInForm form2))
freeVarsInForm (Equi form1 form2) = 
    nub ((freeVarsInForm form1) ++ (freeVarsInForm form2))
freeVarsInForm (Conj forms) = 
    (nub . concat . map freeVarsInForm) forms 
freeVarsInForm (Disj forms) = 
    (nub . concat . map freeVarsInForm) forms 
freeVarsInForm (Forall v form) = delete v (freeVarsInForm form) 
freeVarsInForm (Exists v form) = delete v (freeVarsInForm form) 

map2subst :: [Id] -> (Id -> Term) -> Subst
map2subst dom sigma = [ (x,sigma x) | x <- dom ]

test1 = compose [(xi,y)] [(yi,s[x,y])]
test2 = compose [(xi,a),(yi,a)] [(xi,y)]

